/**
 * Copyright (c) 2010 CWI Amsterdam and others. All rights reserved.
 * This program and the accompanying materials are made available
 * under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 * 
 * Contributors:
 *    CWI Amsterdam - initial API and implementation
 */
package nl.cwi.arne.generator.mcrl2;

import java.util.ArrayList;
import java.util.List;

import nl.cwi.arne.Edge;
import nl.cwi.arne.Node;
import nl.cwi.arne.mcrl2.BasicTerm;
import nl.cwi.arne.mcrl2.Comparator;
import nl.cwi.arne.mcrl2.Comparison;
import nl.cwi.arne.mcrl2.Conjunction;
import nl.cwi.arne.mcrl2.Constraint;
import nl.cwi.arne.mcrl2.Disjunction;
import nl.cwi.arne.mcrl2.Term;

/**
 * @author Christian Krause
 */
public class ArneMCRL2ConstraintFactory {

	/**
	 * Create a list of constraints for a node, based on its incoming arcs.
	 */
	public static List<Term> createNodeConstraint(Node node, NetworkArguments args) {
		List<Term> constraints = new ArrayList<Term>();
		for (Edge edge : node.getIncoming()) {
			int index = node.getNetwork().getNodes().indexOf(edge.getSource());
			if (!edge.getBaseLevels().isEmpty()) {
				Disjunction disjunction = new Disjunction();
				for (Integer baseLevel : edge.getBaseLevels()) {
					Comparison compare = new Comparison(
							new BasicTerm(args.level(index)), Comparator.EQUAL, new BasicTerm(baseLevel));
					disjunction.getChildren().add(compare);
				}
				constraints.add(disjunction);
			} else {
				int level = edge.getEndLevel();
				int delta = level - edge.getStartLevel();
				Comparison compare1 = new Comparison(
						new BasicTerm(args.level(index)), Comparator.EQUAL, new BasicTerm(level));
				Comparison compare2 = new Comparison(
						new BasicTerm(args.delta(index)), Comparator.EQUAL, new BasicTerm(delta));
				constraints.add(new Conjunction(compare1, compare2));
			}
		}
		return constraints;
	}

	/**
	 * Create the fast check for a given node.
	 */
	public static Constraint createFastCheck(Node node, NetworkArguments args) {
		List<Term> constraints = createNodeConstraint(node, args);
		Disjunction disjunction = new Disjunction();
		for (int i=0; i<node.getIncoming().size(); i++) {
			Edge edge = node.getIncoming().get(i);
			if (edge.getBaseLevels().isEmpty()) {
				disjunction.getChildren().add((Constraint) constraints.get(i));
			}
		}
		return disjunction;
	}	
	
}
